\documentclass[a4paper,14pt,russian]{extarticle}

% PDF search & cut'n'paste
\usepackage{cmap}

\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english, russian]{babel}

\usepackage[pdftex]{graphicx}

\usepackage[figurename=Рисунок]{caption} 

\usepackage{algorithmic}

\usepackage{float}

\usepackage{indentfirst} % включить отступ у первого абзаца

% According to GOST, sections should be called chapters in diploma
\usepackage{titlesec}

\titleformat{\section}[block]{\bfseries\large\sffamily\raggedright}
	{Глава~\arabic{section}.}{1ex}{}
\titleformat{\subsection}[block]{\bfseries\normalsize\sffamily\raggedright}
	{\arabic{section}.\arabic{subsection}.}{1ex}{}
\titleformat{\subsubsection}[block]{\normalsize\sffamily\raggedright}
	{\arabic{section}.\arabic{subsection}.\arabic{subsubsection}.}{1ex}{}

\titlespacing*{\section}      {0pt}{3.50ex plus 1ex minus .2ex}{2.3ex plus .2ex}
\titlespacing*{\subsection}   {0pt}{3.25ex plus 1ex minus .2ex}{1.5ex plus .2ex}
\titlespacing*{\subsubsection}{0pt}{3.25ex plus 1ex minus .2ex}{1.5ex plus .2ex}

\usepackage{setspace}
\setstretch{1.5}

\usepackage[titles]{tocloft}

\renewcommand{\cftsecpresnum}{Глава~}
\renewcommand{\cftsecleader}{\bfseries\cftdotfill{\cftdotsep}}
\renewcommand{\cftsecaftersnum}{.}
\renewcommand{\cftsubsecaftersnum}{.}

\newlength{\zyvseclen}
\settowidth{\zyvseclen}{\bfseries\cftsecpresnum\cftsecaftersnum}
\addtolength{\zyvseclen}{2mm}
\addtolength{\cftsecnumwidth}{\zyvseclen}

\renewcommand{\thesection}{\arabic{section}}
\renewcommand{\thesubsection}{\arabic{section}.\arabic{subsection}}
\renewcommand{\thesubsubsection}
        {\arabic{section}.\arabic{subsection}.\arabic{subsubsection}}


\usepackage[top=2cm, bottom=2cm, left=3cm, right=1cm]{geometry}

\global\emergencystretch = .5\hsize

\usepackage{listings}
\usepackage{url}
\usepackage{multirow}

\lstset{% general command to set parameter(s)
	% underlined bold black keywords
	language=[ANSI]C++,
	stringstyle=\ttfamily, % typewriter type for strings
} 
 
\author{Курбацкий Евгений}
\title{Решение SAT на CUDA}


\begin{document}
%emply
%\pagebreak

%emply
%\pagebreak

\renewcommand{\contentsname}{Оглавление}
\tableofcontents 
\pagebreak


\section{Обзор}

\subsection{Введение}

Задача выполнимости булевых формул (SAT\cite{2002} или ВЫП) ---  важная алгоритмическая задача. 

Экземпляром задачи SAT является булева формула, состоящая только из имен
переменных, скобок и операций $\wedge$ (И), $\vee$ (ИЛИ) и $\neg$ (HE). 
Задача заключается в следующем: можно ли назначить всем переменным,
встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.

Согласно теореме Кука, доказанной Стивеном Куком в 1971-м году\cite{Cook1971}, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время от размера записи формулы.

Так как решение  всех NP полных задач можно свести к SAT,
для её решения создаются специальные программы 
SAT решатели. Такие как MinSat\cite{Een}, Chaff\cite{Moskewicz}, PicoSat\cite{Biere2008}. Эти программы применяются во многих областях например в верификации и схемотехнике. Данные программы используют различные эвристики для ускорения работы алгоритма на определенном классе задач. Однако больщенство данных алгоритмов последовательные. Возникает задача увеличения производительности SAT решателя за счет распаралеливания.

\subsubsection{Конъюнктивная нормальная форма}

Дадим три основных определения.

\begin{itemize}
\item
	\textit{Литералом} является либо переменная, либо отрицание переменной. Например, $x$ или $ \neg y$. 
	Для краткости вместо литерала вида $ \neg y$ часто используется переменная с черточкой сверху $ 	\overline y$. 	
\item
	\textit{Дизъюнктом} называется логическое ИЛИ одного или нескольких
	литералов, например $x, x \vee y, x \vee \neg y \vee z $.
\item
	Говорят что формула записана в конъюнктивной нормальной форме (КНФ) (здесь термин "конъюнкция" обозначает логическое И), если переставляет собой логическое И дизъюнктов.
\end{itemize}

 Две булевы формулы называющийся эквивалентными, если имеют одно и то же значение при любой подстановке. Если две формулы эквивалентны, то они либо обе выполнимы, либо обе невыполнимы. Поэтому, на первый взгляд, преобразование произвольных формул в эквивалентные формулы, записанные в КНФ, позволило бы разработать метод полиномиального сведения SAT к КНФ SAT. Однако не все так просто мы действительно можем преобразовать всякую формулу в КНФ, но при таком преобразовании длинна формулы может вырасти экспоненциально. К счастью, приведение произвольной булевой формулы в КНФ --- это лишь одни из возможных способов сведения SAT в КНФ SAT. 

\subsubsection{Преобразование Цейтина}
Преобразование в КНФ, как правило, производится при помощи хорошо известного преобразования Цейтина \cite{1976}, которое генерирует линейное число дополнительных дизъюнктов, а так же линейное число новых переменных, и генерирует эквивалентную формулу (выполнимую тогда и только тогда, когда выполнима исходная формула). Преобразование Цейтина работает за счет добавления новых переменных к формуле, одной на каждую подформулу исходной формулы, вместе с дизъюнктами которые задают отношения между этими новыми переменными и подформулами. 
Например, для формулы
$$ (a \rightarrow (c \wedge d)) \vee (b \rightarrow (c \wedge e)) $$
 будет введена переменная $ f_1 $ определенная как
$ f_1 \leftrightarrow (c \wedge d) $
для того чтобы представить подформулу $(c \wedge d)$. Это определение может быть преобразовано в форме дизъюнктов:
$$ (\neg f_1 \vee c) \wedge (\neg f_1 \vee d) \wedge (\neg c \vee \neg d \vee f_1) $$
Аналогичным образом вводится определение
$ f_2 \leftrightarrow (c \wedge e) $
которое преобразуется в дизъюнкты
$$ (\neg f_2 \vee c) \wedge (\neg f_2 \vee e) \wedge (-c \vee -e \vee f_2) $$
Применение данных определений к исходной формуле сведется 
$ (a \vee f_1) \wedge (b \vee f_2) $
Следующие две переменные будут введены определениями
$ f_3 \leftrightarrow (\neg a \vee f_1)  $ и $ f_4 \leftrightarrow (\neg b \vee f_2) $
и дизъюнктами
$$ (\neg f_3 \vee \neg a \vee f_1) \wedge (a \vee f_3) \wedge (\neg f_1 \vee f_3) \wedge (\neg f_4 \vee \neg b \vee f_2) \wedge (b \vee f_4) \wedge (\neg f_2 \vee f_4) $$
Теперь формула сведется к 
$ (f_3 \vee f_4) $
Вводится последняя переменная 
$ f_5 \leftrightarrow (f_3 \vee f_4) $
и дизъюнкты
$$ (\neg f_5 \vee f_3 \vee f_4) \wedge (\neg f_3 \vee f_5) \wedge (\neg f_4 \vee f_5) $$
Преобразование Цейтина в КНФ линейно относительно длинны исходной формулы, так как операторы, которые появляются в формуле, кодируются фиксированным числом дизъюнктов. Операторы 
and, or, not, nand, nor и implies все имеют конечное кодирование.
На практике мы можем выбрать не вводить некоторые переменные, например $ (f_3 \vee f_4) $ уже в форме дизъюнкта так что нам не требуется определять $ f_5 $.

Ниже по тексту упоминание формулы будет всегда означать формулу в КНФ.

\subsubsection{Алгоритм DPLL}

Алгоритм DPLL(Davis-Putnam-Logemann-Loveland) \cite{Davis1962} является полным алгоритмом основанным на алгоритмом для решения задачи выполнимости формулы пропозициональной  логики в форме КНФ.

Алгоритм был разработан в 1962 году Мартином Дэвисом и Хилари Патнем, Дэвисом, Джорджем Логеманом и Дональдом Лавлендом, и это расширение раннего алгоритма Девиса-Патнема, который являлся основанной на резолюции процедурой разработанной Девисом и Патнем в 1960-м году. 

DPLL --- это крайне эффективная процедура и после более 40 лет все еще формирует базис для более эффективных полных SAT решателей, так же как и для многих систем автоматического доказательства теорем.
Ниже приводится псевдокод алгоритма DPLL. 

%\begin{singlespacing}
%\begin{algorithm}[H]
%\KwData{ CNF $F$ }
%\KwResult{ множество литералов или UNSATISFIABLE }
%	$(I, F) = unit-resolition(F)$\;
%	\uIf{ $F = \{\}$ } {
%		\Return $I$\;		
%	} \uElseIf {$\{\} \in F$} {
%		\Return UNSATISFIABLE\;		
%	} \Else{
%		choose variable $V$ from $F$\;
%		\uIf{ $ R = DPLL(F[V=1]) \neq UNSATISFIABLE $ } {
%			\Return $R \cup I \cup \{V\}$\;		
%		} \uElseIf {$ R = DPLL(F[V=0]) \neq UNSATISFIABLE $} {
%			\Return $R \cup I \cup \{\neg V\}$\;		
%		} \Else{
%			\Return UNSATISFIABLE\;
%	            }
%            }
%\caption{Алгоритм DPLL \label{DPLL}}
%\end{algorithm}
%\end{singlespacing}


\begin{singlespacing}
\begin{algorithmic}[1]
\STATE $(I, F) \leftarrow unit~resolition(F)$
\IF{$F = \{\}$}
	\RETURN $I$
\ELSIF{$\{\} \in F$}
	\RETURN $UNSATISFIABLE$
\ELSE
	\STATE choose variable $V$ from $F$
	\IF{$R = DPLL(F[V=1]) \neq UNSATISFIABLE$}
		\RETURN $R \cup I \cup \{V\}$
	\ELSIF{$R = DPLL(F[V=0]) \neq UNSATISFIABLE$}
		\RETURN $R \cup I \cup \{\neg V\}$
	\ELSE
		\RETURN $UNSATISFIABLE$
	\ENDIF
\ENDIF
\end{algorithmic}
\end{singlespacing}

Основная идея алгоритма DPLL заключается в том, что формула $F$ выполнима, тогда и только тогда когда для любой переменной x содержащейся в $F$ выполнима одна из формул: $F[x = 0]$ или $F[x = 1]$. Причем, каждая из этих формул меньше исходной $F$. Таким образом, проверку выполнимости можно свести к рекурсивной процедуре.
Для сокращения формулы на первом шаге алгоритма используется операция удаления единичных дизъюнктов. Единичным дизъюнктом называется дизъюнкт состоящий из одного литерала. Пусть в формуле есть дизъюнкт вида $ \{ x_i \} $. Тогда формула вида $ F[x_i = 0] $  невыполнима так как содержит пустой дизъюнкт. Следовательно вместо формулы F можно использовать формулу $ F[x_i = 1] $. Аналогично сокращается формула содержащая единичный дизъюнкт $ \{ \neg x_i \} $. Эта операция повторяется до тех пор пока формуле не останется единичных дизъюнктов.

Если после этого появляются пустые дизъюнкты, значит формула $F$ невыполнима. Далее выбирается переменная $V$ и проверяется выполнима ли формула при присвоении этой переменной значения истина. Если нет то, проверяется выполнима ли формула при присвоении этой переменной значения ложь. 
Если ни одна из формул $F[V = 0]$, $F[V = 1]$ не выполнима, следовательно, исходная формула не выполнима.

\subsubsection{Алгоритм Look-Ahead}

В алгоритме DPLL выбирается некоторая переменная $x$ после чего задача $f$ разбивается на $f[x = 0]$ и $f[x=1]$. Как правило на практике выбор переменной $x$ значительно влияет на время выполнения программы. Возникает идея вычислить фиксирование какой из переменных наиболее выгодно. На этой идее основан алгоритм DPLL Look Ahead \cite{Bohm1996}. Алгоритм для каждой переменной $x$ содержащаяся в формуле $f$ выполняет операцию удаления единичных дизъюнктов.
На рис.~\ref{fig:LookAheadTree} схематично изображена идея алгоритма Look Ahead.

\begin{figure}[H]
	\centering
	\includegraphics[width=90mm]{pics/LookAheadTree.pdf}
	\caption{Демонстрация работы Look-Ahead алгоритма}
	\label{fig:LookAheadTree}
\end{figure}

В алгоритме DPLL за счет удаления единичных дизъюнктов мы можем находить значение некоторых переменных "бесплатно". Для данных переменных не требуется пробовать оба значения, что значительно ускоряет время выполнения алгоритма. Когда алгоритм разделяет формулу $f$ на две $f[x_i=0]$ и $f[x_i=1]$ можно использовать любую переменную $x_i$.  Алгоритму более выгодно выбирать переменную присвоение которой дает большее количество единичных дизъюнктов. 
Ниже приводится псевдокод алгоритма Look-Ahead DPLL.

%\begin{singlespacing}
%\begin{algorithm}[H]
%\KwData{ CNF $F$ }
%\KwResult{ SATISFIABLE или UNSATISFIABLE }
%
%	\If{ $F = \emptyset$ } {
%		\Return SATISFIABLE\;		
%	} 
%	$<F; x_{decisiopn}>$ := LookAhead($F$) 
%
%	\uIf{  $\{\} \in F $ } {
%		\Return UNSATISFIABLE\;
%	} \ElseIf {no $x_{decisiopn}$ is selected} {
%		\Return LookAhead-DPLL(F)\;		
%	} 
%            B := DirectionHeuristic($x_{decisiopn}$; F)\;
%            \If {LookAhead-DPLL(F[$x_{decision} = B $]) = SATISFIABLE} {
%            	\Return SATISFIABLE\;
%	}
%	\Return LookAhead-DPLL(F[$x_{decision} = \neg B$])\;
%
%\caption{Алгоритм DPLL Look-Ahead \label{Look-Ahead}}
%\end{algorithm}
%\end{singlespacing}

\begin{singlespacing}
\textbf{Функция} Look Ahead DPLL($F$)
\begin{algorithmic}[1]
\IF{$F = \{\}$}
	\RETURN $SATISFIABLE$
\ENDIF
\STATE $(F, x_{decisiopn}) \leftarrow$Look Ahead($F$)
\IF{$\{\} \in F$}
	\RETURN $UNSATISFIABLE$
\ELSIF{no $x_{decisiopn}$ is selected} 
	\RETURN Look~Ahead~DPLL($F$)
\ENDIF
\STATE $B \leftarrow$ DirectionHeuristic($x_{decisiopn}$; $F$)
\IF {Look Ahead DPLL($F[x_{decision} = B ]$) = SATISFIABLE} 
	\RETURN SATISFIABLE
\ENDIF
\RETURN Look Ahead DPLL($F[x_{decision} = \neg B]$)
\end{algorithmic}
\end{singlespacing}

%\begin{singlespacing}
%\begin{algorithm}[H]
%\KwData{ formula $F$ }
%\KwResult{ SATISFIABLE или UNSATISFIABLE }
%	$P$ := Preselect($F$) \;
%	\For  {x $\in P$} {
% 		F := Lool Ahead Reasoning($F, x$)\;
%		\uIf {empty clause $ \in F[x = 0]$ and empty clause $\in F[x = 1] $} {
%			\Return $<F[X=0]; *>$ \;
%		} \uElseIf {empty clause $ \in F[x = 0]$} {
%  			$F := F[x = 1]$ \;
%		} \uElseIf {empty clause $ \in F[x = 1]$} {
% 			$F := F[x = 0]$ \;
%		} \Else {
% 			h(x) :=   DecisionHeuristic($ F , F[x = 0], F[x = 1] $) \;
%		}
%            } 
%	\Return  < $F$; $x$ with greatest $H(x)$> \;
%
%\caption{Функция LookAhead \label{function-Look-Ahead}}
%\end{algorithm}
%\end{singlespacing}

\begin{singlespacing}
\textbf{Функция} Look Ahead($F$)
\begin{algorithmic}[1]
\STATE $P \leftarrow $ Preselect($F$) 
\FOR{x $\in P$} 
	\STATE $F \leftarrow$ Lool Ahead Reasoning($F, x$)
	\IF{empty clause $ \in F[x = 0]$ and empty clause $\in F[x = 1] $}
		\RETURN $(F[X=0], *)$
	\ELSIF{empty clause $ \in F[x = 0]$}
		\STATE $F := F[x = 1]$ 
	\ELSIF{empty clause $ \in F[x = 1]$}
		\STATE $F := F[x = 0]$ 
	\ELSE
		\STATE h($x$) $\leftarrow$ DecisionHeuristic($ F , F[x = 0], F[x = 1] $) 
	\ENDIF
	\RETURN  ($F$, $x$ with greatest $H(x)$) 
\ENDFOR
\end{algorithmic}
\end{singlespacing}

Опишем функицю Look-Ahead. Для каждой переменной $x$ вычисляется $F[x=0]$ и $F[x=1]$. Проверяются следующие условия: 

\begin{itemize}
\item 
	Если обе формулы содержат пустой дизъюнкт, то формула F будет невыполнима.
\item 
	Если F[x=0] содержит конфликт, то формула F эквивалентна F[x=1].
\item 
	Если F[x=1] содержит конфликт, то формула F эквивалентна F[x=0].
\item 
	Иначе вычисляется некоторое число, вес характеризующий переменную x.
\end{itemize}

После чего в качестве переменной для расщепления выбирается переменная с наибольшим весом.
Данная эвристика считается наиболее подходящей для сложных случайных формул.


\subsubsection{Получение новых дизъюнктов из конфликтов}

Одна из главных причин распространенности использования SAT во многих приложениях состоит в том, что 
решатели основанные на изучении дизъюнктов из конфликтов (Conflict-Driven Clause Learning) крайне эффективны на практике. Впервые данная эвристика была предложена в работе \cite{Marques-Silva1999}.  Решатель, получающий новые дизъюнкты из конфликтов кране похож на простой DPLL решатель. Он выполняет одну  дополнительную операцию. При возникновении конфликта, ситуации, когда в формуле появляется пустой дизъюнкт, решатель выполняет операцию анализа конфликта.

% In the context of search algorithms for SAT, variables can be assigned a logic value, either 0 or 1. Alternatively, variables may also be unassigned. Assignments to the problem variables can be defined as a function ν : X → {0, u, 1}, where u denotes an undefined value used when a variable has not been assigned a value in  {0, 1}. Given an assignment ν, if all variables are assigned a value in {0, 1}, then ν is referred to as a complete assignment. Otherwise it is a partial assignment.

% Clauses are characterized as unsatisfied, satisfied, unit or unresolved. A clause is unsatisfied if all its literals are assigned value 0. A clause is satisfied if at least one of its literals is assigned value 1. A clause is unit if all literals but one are assigned value 0, and the remaining literal is unassigned. Finally, a clause is unresolved if it is neither unsatisfied, nor satisfied, nor unit.


Данная операция заключается в том что алгоритм пытается найти меньшую частичную подстановку переменных $\{x_{i_1} = v_1, x_{i_2}=v_2, x_{i_3} = v3, ...\}$, которая вызывает данный конфликт. Так как эта подстановка невозможна, то в формулу можно добавить новый дизъюнкт, который не будет выполним при данной подстановке. Для этого дя каждого присваивания $ x_i = 1 $ в дизъюнкт добавляется литерал $ \neg x_i $, а для $ x_i = 0 $ в дизъюнкт добавляется литерал $ x_ i $. 

 В результате данной операции решатель получает новый дизъюнкт d, такой что при добавлении данного дизъюнкта к формуле её свойство выполнимости не изменяется. 

Рассмотрим данный алгоритм на примере формулы f. 

$$ f = (x1 \vee \neg x2) \wedge (x2 \vee x3) \wedge (x2 \vee \neg x4) \wedge (\neg x1 \vee \neg x3 \vee x4) $$

Если подставить значения переменных $ x_1 = 1 $ и $ x_2 = 0 $, то за счет удаления единичных дизъюнктов будут выведены значения переменных $ x_3 = 1 $ и $ x_4 = 0 $. После чего случится конфликт, будет не удовлетворен дизъюнкт $ (\neg x1 \vee \neg x3 \vee x4) $. На рис.~\ref{fig:Implication} указан граф зависимостей для данного конфликта. Из данного графа видно что значения переменных $x_3 , x_4$ выводятся из переменной $x_2$. Соответственно данный конфликт происходит только из изначального присваивания $ x_1 = 1 $ и $ x_2 = 0 $. Соответственно в формулу можно добавить новый дизъюнкт $(\neg x1 \vee  x2)$. 

 \begin{figure}[H]
	\centering
	\includegraphics[width=80mm]{pics/Implication.pdf}
	\caption{Демонстрация работы Look-Ahead алгоритма}
	\label{fig:Implication}
\end{figure}


\subsection{Параллельные алгоритмы}

В работе \cite{Hamadi} приводится обзор различных параллельных алгоритмов для решения SAT.

\subsubsection{Параллельное удаление единичных дизъюнктов}

В \cite{Kasif1990} рассматривается наиболее простой вариант для распараллеливания --- это параллельное удаление единичных дизъюнктов.
Так как удаление единичных дизъюнктов можно производить независимо, то эту операцию можно
 распределить. Но на практике это оказывается крайне неэффективно так как количество дизъюнктов которые можно удалять параллельно варьируется от задачи к задаче.

\subsubsection{Разделяй и властвуй}

 \begin{figure}[H]
	\centering
	\includegraphics[width=170mm]{pics/DPLLtree.pdf}
	\caption{Дерево обхода для DPLL}
	\label{fig:DPLLTree}
\end{figure}

 \begin{figure}[H]
	\centering
	\includegraphics[width=170mm]{pics/DPLLtree2.pdf}
	\caption{Дерево обхода для DPLL разделенное на две части}
	\label{fig:DPLLTree2}
\end{figure}

  Алгоритм DPLL является рекурсивным. При этом задача нахождения удовлетворяющего набора 
  разделяет на две независимые подзадачи. Эти подзадачи в свою очередь разделяются еще на две.
  Таким образом мы можем решать эти задачи независимо. При применение данного метода возникает
  проблема в том что две подзадачи могут иметь не равный объем. 
 
\subsubsection{Обмен изученными дизъюнктами}

  В работе \cite{Chrabakh2003} рассматривается реализация SAT-решателя GrADSAT с применением технологии GRID. При этом применяется метод разделяй и властвуй. При этом каждый из решателей использует алгоритм для получение новых дизъюнктов. Для ускорения работы используется обмен изученными
  дизъюнктами.  Полученные от других решателей дизъюнкты обрабатываются следующим образом:
\begin{itemize}
\item
Если дизъюнкт имеет только один не присвоенный литерал производится вывод значения переменной.
\item
Если в дизъюнкте несколько не присвоенных литералов, то дизъюнкт просто сохраняется в базе.
\item
Если в дизъюнкте все литералы ложные то текущая формула не выполнима.
\item
Если дизъюнкт имеет значение истина то он не заносится в базу так как не ограничивает пространство поиска.
\end{itemize}
Данный подход не всегда работает хорошо, например при большом количестве клиентов затраты на обмен дизъюнктами могут значительно превышать пользу. Что бы избежать этого  GrADSAT обмениваются только короткими дизъюнктами, для того чтобы снизить затраты на обмен.  Так же короткие дизъюнкты больше сокращают пространство поиска. 

\subsubsection{Параллельный запуск нескольких решателей с разными параметрами}

В работе ManySat\cite{Hamadi} используется подход при котором запускается несколько независимых решателей SAT. При этом
каждый из них решает задачу от начала до конца. При этом каждый решатель запускается с разными параметрами.
Время работы решателя равно времени работы самого быстрого потока. Так как скорость работы решателя сильно зависит от параметров, то шанс что один из потоков решит задачу быстрее, чем если бы он решал часть задачи методом разделения всего пространства решений. 

\subsection{Технология CUDA}

\subsubsection{Разница между CPU и GPU в параллельных расчётах}
Рост частот универсальных процессоров упёрся в физические ограничения и высокое энергопотребление, и увеличение их производительности всё чаще происходит за счёт размещения нескольких ядер в одном чипе. В чипах NVIDIA основной блок — это мультипроцессор с восемью-десятью ядрами и сотнями ALU в целом, несколькими тысячами регистров и небольшим количеством разделяемой общей памяти. Кроме того, видеокарта содержит быструю глобальную память с доступом к ней всех мультипроцессоров, локальную память в каждом мультипроцессоре, а также специальную память для констант. 

Ядра мультипроцессора в GPU являются SIMD (одиночный поток команд, множество потоков данных) ядрами. И эти ядра исполняют одни и те же инструкции одновременно, такой стиль программирования является обычным для графических алгоритмов и многих научных задач, но требует специфического программирования. Зато такой подход позволяет увеличить количество исполнительных блоков за счёт их упрощения. 
Итак, перечислим основные различия между архитектурами CPU и GPU. 

Ядра CPU созданы для исполнения одного потока последовательных инструкций с максимальной производительностью, а GPU проектируются для быстрого исполнения большого числа параллельно выполняемых потоков инструкций. 

Кроме того, на видеокартах применяется более быстрая память, и в результате видеочипам доступна в разы большая пропускная способность памяти, что также весьма важно для параллельных расчётов, оперирующих с огромными потоками данных. 

Есть множество различий и в поддержке многопоточности. CPU исполняет 1-2 потока вычислений на одно процессорное ядро, а видеочипы могут поддерживать до 1024 потоков на каждый мультипроцессор, которых в чипе несколько штук. 

Кроме того, центральные процессоры используют SIMD (одна инструкция выполняется над многочисленными данными) блоки для векторных вычислений, а видеочипы применяют SIMT (одна инструкция и несколько потоков) для скалярной обработки потоков. SIMT не требует, чтобы разработчик преобразовывал данные в векторы, и допускает произвольные ветвления в потоках. 

Вкратце можно сказать, что в отличие от современных универсальных CPU, видеочипы предназначены для параллельных вычислений с большим количеством арифметических операций. И значительно большее число транзисторов GPU работает по прямому назначению — обработке массивов данных, а не управляет исполнением (flow control) немногочисленных последовательных вычислительных потоков. На рис.~\ref{fig:cpu_vs_gpu} изображена схема того, сколько места в CPU и GPU занимает разнообразная логика. 

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/cpu_vs_gpu.png}
	\caption{Схема устройства процессров GPU и CPU}
	\label{fig:cpu_vs_gpu}
\end{figure}


В итоге, основой для эффективного использования мощи GPU в  распараллеливание алгоритмов на сотни исполнительных блоков, имеющихся в видеочипах. 

В результате всех описанных выше отличий, теоретическая производительность видеочипов значительно превосходит производительность CPU. Компания NVIDIA приводит такой график роста производительности CPU и GPU за последние несколько лет на рис.~\ref{fig:gflops}.

\begin{figure}[H]
	\centering
	\includegraphics[width=130mm]{pics/gflops.png}
	\caption{График роста производительности GPU и CPU}
	\label{fig:gflops}
\end{figure}

 
Естественно, на CPU гораздо проще на практике достичь теоретических цифр, да и цифры приведены для одинарной точности в случае GPU, и для двойной — в случае CPU. В любом случае, для части параллельных задач одинарной точности хватает, а разница в скорости между универсальными и графическими процессорами весьма велика, и поэтому овчинка стоит выделки. 


\subsubsection{Преимущества и ограничения CUDA}
Программно-аппаратная архитектура для вычислений на GPU компании NVIDIA отличается от предыдущих моделей GPGPU тем, что позволяет писать программы для GPU на настоящем языке Си со стандартным синтаксисом, указателями и необходимостью в минимуме расширений для доступа к вычислительным ресурсам видеочипов. 
Преимущества CUDA перед традиционным подходом к GPGPU вычислениям: 

\begin{itemize}
\item
	интерфейс программирования приложений CUDA основан на стандартном языке программирования Си с расширениями, что упрощает процесс изучения и внедрения архитектуры CUDA;
\item 
	CUDA обеспечивает доступ к разделяемой между потоками памяти размером в 16 Кб на мультипроцессор, которая может быть использована для организации кэша с широкой полосой пропускания, по сравнению с текстурными выборками;
\item 
	более эффективная передача данных между системной и видеопамятью
\item 
	отсутствие необходимости в графических API с избыточностью и накладными расходами;
\item 
	линейная адресация памяти, и gather и scatter, возможность записи по произвольным адресам;
\item 
	аппаратная поддержка целочисленных и битовых операций.
\end{itemize}

Основные ограничения CUDA: 

\begin{itemize}
\item 
	отсутствие поддержки рекурсии для выполняемых функций;
\item 
	минимальная ширина блока в 32 потока;
\item 
	закрытая архитектура CUDA, принадлежащая NVIDIA.
\end{itemize}

Основные преимущества CUDA по сравнению с предыдущими методами GPGPU вытекают из того, что эта архитектура спроектирована для эффективного использования неграфических вычислений на GPU и использует язык программирования C, не требуя переноса алгоритмов в удобный для концепции графического конвейера вид. CUDA предлагает новый путь вычислений на GPU, не использующий графические API, предлагающий произвольный доступ к памяти. 

\subsubsection{Модель программирования CUDA}

Повторимся, что CUDA использует параллельную модель вычислений, когда каждый из SIMD процессоров выполняет ту же инструкцию над разными элементами данных параллельно. GPU является вычислительным устройством, сопроцессором (device) для центрального процессора (host), обладающим собственной памятью и обрабатывающим параллельно большое количество потоков. Ядром (kernel) называется функция для GPU, исполняемая потоками (аналогия из 3D графики — шейдер). 

Мы говорили выше, что видеочип отличается от CPU тем, что может обрабатывать одновременно десятки тысяч потоков, что обычно для графики, которая хорошо распараллеливается. Каждый поток скалярен, не требует упаковки данных в 4-компонентные векторы, что удобнее для большинства задач. Количество логических потоков и блоков потоков превосходит количество физических исполнительных устройств, что даёт хорошую масштабируемость для всего модельного ряда решений компании. 

Модель программирования в CUDA предполагает группирование потоков. Потоки объединяются в блоки потоков (thread block) — одномерные или двумерные сетки потоков, взаимодействующих между собой при помощи разделяемой памяти и точек синхронизации. Программа (ядро, kernel) исполняется над сеткой (grid) блоков потоков (thread blocks), см. рисунок ниже. Одновременно исполняется одна сетка. Каждый блок может быть одно-, двух- или трехмерным по форме, и может состоять из 512 потоков на текущем аппаратном обеспечении.  На рис.~\ref{fig:cuda3} схематично изображена модель выполнениея программы на CUDA.

\begin{figure}[H]
	\centering
	\includegraphics[width=90mm]{pics/cuda3.png}	
	\caption{Схема выполнения программы на CUDA}
	\label{fig:cuda3}
\end{figure}
 
Блоки потоков выполняются в виде небольших групп, называемых варп (warp), размер которых — 32 потока. Это минимальный объём данных, которые могут обрабатываться в мультипроцессорах. И так как это не всегда удобно, CUDA позволяет работать и с блоками, содержащими от 64 до 512 потоков. 

Группировка блоков в сетки позволяет уйти от ограничений и применить ядро к большему числу потоков за один вызов. Это помогает и при масштабировании. Если у GPU недостаточно ресурсов, он будет выполнять блоки последовательно. В обратном случае, блоки могут выполняться параллельно, что важно для оптимального распределения работы на видеочипах разного уровня, начиная от мобильных и интегрированных. 
Модель памяти CUDA

На рис.~\ref{fig:cuda5} изображена модель памяти CUDA. Модель памяти в CUDA отличается возможностью побайтной адресации, поддержкой как gather, так и scatter. Доступно довольно большое количество регистров на каждый потоковый процессор, до 1024 штук. Доступ к ним очень быстрый, хранить в них можно 32-битные целые или числа с плавающей точкой. 

\begin{figure}[H]
	\centering
	\includegraphics[width=90mm]{pics/cuda5.png}
	\caption{Модель памяти CUDA}
	\label{fig:cuda5}
\end{figure}


Каждый поток имеет доступ к следующим типам памяти: 
\begin{itemize}
\item 
	Глобальная память — самый большой объём памяти, доступный для всех мультипроцессоров на видеочипе, размер составляет от 256 мегабайт до 1.5 гигабайт на текущих решениях (и до 4 Гбайт на Tesla). Обладает высокой пропускной способностью, более 100 гигабайт/с для топовых решений NVIDIA, но очень большими задержками в несколько сот тактов. Не кэшируется, поддерживает обобщённые инструкции load и store, и обычные указатели на память. 
\item 
	Локальная память — это небольшой объём памяти, к которому имеет доступ только один потоковый процессор. Она относительно медленная — такая же, как и глобальная. 
Разделяемая память — это 16-килобайтный (в видеочипах нынешней архитектуры) блок памяти с общим доступом для всех потоковых процессоров в мультипроцессоре. Эта память весьма быстрая, такая же, как регистры. Она обеспечивает взаимодействие потоков, управляется разработчиком напрямую и имеет низкие задержки. Преимущества разделяемой памяти: использование в виде управляемого программистом кэша первого уровня, снижение задержек при доступе исполнительных блоков (ALU) к данным, сокращение количества обращений к глобальной памяти. 
\item 
	Память констант — область памяти объемом 64 килобайта (то же — для нынешних GPU), доступная только для чтения всеми мультипроцессорами. Она кэшируется по 8 килобайт на каждый мультипроцессор. Довольно медленная — задержка в несколько сот тактов при отсутствии нужных данных в кэше. 
\item
	Текстурная память — блок памяти, доступный для чтения всеми мультипроцессорами. Выборка данных осуществляется при помощи текстурных блоков видеочипа, поэтому предоставляются возможности линейной интерполяции данных без дополнительных затрат. Кэшируется по 8 килобайт на каждый мультипроцессор. Медленная, как глобальная — сотни тактов задержки при отсутствии данных в кэше. 

\end{itemize}

Естественно, что глобальная, локальная, текстурная и память констант — это физически одна и та же память, известная как локальная видеопамять видеокарты. Их отличия в различных алгоритмах кэширования и моделях доступа. Центральный процессор может обновлять и запрашивать только внешнюю память: глобальную, константную и текстурную. 

\begin{figure}[H]
	\centering
	\includegraphics[width=90mm]{pics/cuda4.png}
	\caption{Модель доступа к памяти CUDA}
	\label{fig:cuda4}
\end{figure}

 
Из написанного выше понятно, что CUDA предполагает специальный подход к разработке, не совсем такой, как принят в программах для CPU. Нужно помнить о разных типах памяти, о том, что локальная и глобальная память не кэшируется и задержки при доступе к ней гораздо выше, чем у регистровой памяти, так как она физически находится в отдельных микросхемах. 
Типичный, но не обязательный шаблон решения задач: 
\begin{itemize}
\item 
	задача разбивается на подзадачи;
\item 
	входные данные делятся на блоки, которые вмещаются в разделяемую память;
\item 
	каждый блок обрабатывается блоком потоков;
\item 
	подблок подгружается в разделяемую память из глобальной;
\item 
	над данными в разделяемой памяти проводятся соответствующие вычисления;
\item 
	результаты копируются из разделяемой памяти обратно в глобальную.
\end{itemize}

\subsubsection{Оптимизация программ на CUDA}

В общих чертах, при оптимизации программы CUDA нужно постараться добиться оптимального баланса между размером и количеством блоков. Большее количество потоков в блоке снизит влияние задержек памяти, но снизит и доступное число регистров. Кроме того, блок из 512 потоков неэффективен, сама NVIDIA рекомендует использовать блоки по 128 или 256 потоков, как компромиссное значение для достижения оптимальных задержек и количества регистров. 

Среди основных моментов оптимизации программ CUDA: как можно более активное использование разделяемой памяти, так как она значительно быстрее глобальной видеопамяти видеокарты; операции чтения и записи из глобальной памяти должны быть объединены (coalesced) по возможности. Для этого нужно использовать специальные типы данных для чтения и записи сразу по 32/64/128 бита данных одной операцией. Если операции чтения трудно объединить, можно попробовать использовать текстурные выборки. 

\subsubsection{Постановка задачи}

Рассмотрим существующие подходы к решению SAT на GPU. В \cite{Manolios2006} описывается реализвация  survey propagation\cite{Braunstein2002} на GPU.  В \cite{Deleau} описанно программное средсво GPU4SAT использующее матричный метод для решения SAT. В \cite{Zhongwen2005} описывается реализация генестического алгоритма на GPU для решение задачи 3-SAT.

Все вышеперечисленные подходы не обладают полнотой. В связи с этим возникает задача исследования возможности создания полного SAT решателя на GPU.

Предлагается реализовать разработать алгоритм для решения задачи выполнимости с применением технологии CUDA. 
В работе предлагается попробовать несколько подходов к реализации SAT решателя описанных выше.
\begin{enumerate}
\item
	Параллельное удаление единичных дизъюнктов.
\item
	Разделение задачи на независимые подзадачи.
\item
	Параллельная реализация эвристики Look Ahead.
\item
	Разделение пространства поиска меду разными решателями с изучением новых дизъюнктов.
\item
	Параллельный запуск независимых решателей.
\end{enumerate}
Для распаривания предлагается разделять различные поддеревья между разными потоками.

Этапы работы:
\begin{enumerate}
\item
	Реализация последовательного алгоритма DPLL. В связи с тем, что большинство современных решателей SAT содержат большое число эвристик, предлагается реализовать более простую версию алгоритма на языке С. 
\item
	Оптимизация при помощи CUDA. Предлагается перенести наиболее требовательные к ресурсам этапы работы алгоритма на платформу CUDA.
\item
	Анализ ускорения получаемого при применении технологии CUDA.
\end{enumerate}

\pagebreak

\section{Реализация задачи выполнимости на CUDA}

\subsection{Подходы к реализация SAT}

Выше был описан общий вид алгоритма DPLL, не отражающий особенностей реализации, ниже буду рассматриваться особенности переноса данного алгоритма на CUDA. Так как архитектура CUDA значительно отличается от CPU было испробовано несколько подходов к реализации SAT на CUDA для того что бы выбрать наиболее подходящий для данной платформы. На  рис.~\ref{fig:tries} изображена схема испробованных подходов к реализации SAT.

\begin{figure}[H]
	\centering
	\includegraphics[width=140mm]{pics/Algorithms.pdf}
	\caption{Схема различных подходов к реализации SAT на CUDA}
	\label{fig:tries}
\end{figure}

На схеме представлены следующие методы:

\begin{itemize}
\item
	Разделяй и властвуй --- самый простой метод распараллеливания, используется как основа для других методов.
\item
	Разделяй и властвуй с изучением новых дизъюнктов --- метод использует популярную эвристику получения новых дизъюнктов из конфликтов. Все потоки используют общую базу для хранения формулы, как следствие реализуется обмен дизъюнктами. 
\item
	Look-Ahead --- Реализует простой алгоритм Look-Ahead DPLL, в котором каждая переменная обрабатываться в отдельном потоке.
\item
	Разделяй и властвуй c Look-Ahead --- комбинируется подходы Look-Ahead и разделяй и властвуй для улучшения производительности, счет увеличения количества потоков которые можно запустить одновременно.
\end{itemize}

Рассмотрим основные требования к реализация алгоритмов на CUDA:
\begin{itemize}
\item
	Реализация не должна иметь сложных структур данных. 
\item
	Она не должна содержать в себе рекурсивных процедур. А так же процедур с большим количеством ветвлений. 	
\end{itemize}

Ниже распишем подробно как адаптировать алгоритм DPLL для реализации на CUDA.

\subsection{Хранение формулы}

В связи с тем что расстреливание алгоритма предполагает параллельный запуск большого числа решателей, то требуется хранить состояние решателя наиболее компактно. Для работы алгоритма DPLL можно не хранить значение формулы $ f[x_{i_1} = v_1, x_{i_2} = v_2, …] $ в текущем состоянии непосредственно. 

Вместо текущего вида формулы решатель хранит исходную формулу f и массив $variables$, в котором для каждой переменной $ x_i $ хранится её значение $ v_i $: один, ноль или "UNASSIGNED" (если значение переменной еще не определено). 
Текущая формула $f[x_{i_1} = v_1, x_{i_2} = v_2, …]$ вычисляется на лету  из изначальной формулы и массива $variables$. 

Чтобы использовать как можно более простую структуру данных для хранения формулы вся формула хранится в  одном линейном массиве. В котором записана последовательность дизъюнктов.
Каждый дизъюнкт представляет собой последовательность литералов,  заканчивающуюся минус единицей. 

Литерал хранится в виде одного числа, в следующем формате. В младшем бите храниться наличие отрицания перед литералом. Один --- есть отрицание, ноль --- нет. В старших битах храниться номер переменной. Переменные нумеруются с нуля.

Для того чтобы сослаться на дизъюнкт используется ссылка на его первый литерал. Например формула:
$$  (x1 \vee  \neg x5 \vee  x4) \wedge  (\neg x1 \vee  x5 \vee  x3 \vee  x4) \wedge (\neg x3 \vee  \neg x4) $$
будет записана в виде:  \texttt{0, 9, 6, -1, 3, 8, 4, 6, -1, 5, 7, -1}.\\
В формуле будут дизъюнкты: \texttt{0, 4, 9}.

Решатель хранит для каждого литерала список дизъюнктов в которых он содержится, для того чтобы быстро находить необходимые дизъюнкты.

В алгоритме DPLL необходимо уметь находить в формуле дизъюнкты размером один или пустые. Для того чтобы вычислить текущий вид дизъюнкта требуется пройти по всем его литералам. Если хоть один из литералов дизъюнкта имеет значение истина, то и весь дизъюнкт имеет значение истина и его можно не учитывать. Иначе для получения текущего вида дизъюнкта требуется  учитывать только те литералы значение которых не присвоено. Если в дизъюнкт оказался пустым следовательно текущую формулу удовлетворить невозможно. Если все литералы кроме одного назовем его $l$ не удовлетворены, то такой дизъюнкт называется единичным. Единственный способ удовлетворить единичный дизъюнкт это присвоить значение переменной $varaible(l)$ так что бы значение $l$ стало истина. Таким образом вычисляются новые значения переменных.

Ниже приведена часть программы выполняющая проверку дизъюнкта.
\begin{singlespacing}
\begin{lstlisting}[language=C++]
__device__
int calculateUnit(int clauseNum, int *varValues) {
    int unit = -1;

    for (int i = clauseNum;; i++) {
        int var = tex1Dfetch(clauses_tex, i);
        if (var == -1) {
            break;
        }
        int value = varValues[var >> 1];

        if (value == -1) {
            if (unit != -1) {
                return -2;
            } else {
                unit = var;
            }
        }
        if (value == var) {
            return -2;
        }
    }
    return unit;
}
\end{lstlisting}
\end{singlespacing}

\subsection{Структуры данных}

Все реализации DPLL, описанные ниже, используют некоторый общий набор переменных. Для того что бы не останавливаться на них в дальнейшем опишем основные структуры данных которые используются 
алгоритмом.

Реализация DPLL использует следующие переменные:
\begin{itemize}
\item
  variables --- значения переменных {0, 1, UNASSIGNED}.
\item
  stack --- последовательность присвоение переменных.
\item
  stackSize --- размер стека.
\item
  reason --- причина по которой значение было присвоено Для того что бы построить граф зависимостей. Решатель использует массив reasons. Для каждой переменной массив reasons содержит одно из следующих значений:
 
\begin{itemize}
\item
	Номер единичного дизъюнкта, при удалении которого выведено значение данной переменной
\item
	Значение было выбрано для расщепления
\item
	Значение было присвоено после того как формула с другим значением оказалась невыполнимой.
\end{itemize}

\end{itemize}

Ниже приводится базовый алгоритм DPLL.

%\begin{singlespacing}
%\begin{algorithm}[H]
%	\KwData{ CNF $F$ }
%	\KwResult{ множество литералов или UNSAT }   
%	\While{watchedSize < variablesNumber}{
%            	\If{need var guess}{
% 			guess var() \;
%            	}
%            	propagateConstaints() \;
%		\If{ not  rollback()}{
%                   		\Return UNSAT \;
%	            }
%	    }
%	    \Return variables \;
%\caption{DPLL \label{function-Look-Ahead}}
%\end{algorithm}
%\end{singlespacing}

\begin{singlespacing}
\textbf{Функция} DPLL
\begin{algorithmic}[1]
\WHILE{$watchedSize < variablesNumber$} 
	\IF{need var guess}
		\STATE guess var();
	\ENDIF
	\STATE propagate constrains();
	\IF{$ \neg $ rollback()}
		\RETURN UNSAT
	\ENDIF
\ENDWHILE
\RETURN varaibles
\end{algorithmic}
\end{singlespacing}

\subsection{Метод разделяй и властвуй}

Метод разделяй и властвуй является базовым методом для распараллеливания DPLL. Как уже опивалось выше он заключается в том, что различные подзадачи алгоритма DPLL запускаются в отдельных потоках.

CUDA поддерживает запуск одного ядра с разным набором данных для разных потока. Удобно представить эти потоки как пул решателей каждый из которых решает подзадачу SAT. При этом некоторые решатели могут быть неактивны. Если один решатель находит ответ, алгоритм останавливается и возвращает его. Если решатель не находит ответа то он останавливается. Если все решатели завершаются, алгоритм  возвращает UNSAT. 

При попытке разделить пространство поиска на части, возникает проблема балансировки. Различные подформулы возникающие при подстановке переменных могут иметь различную вычислительную трудность. В связи с этим разные потоки могут закончить свою работу намного раньше остальных. При этом вычислительный ресурс будет использован не эффективно. Чтобы такого не происходило разделение операций между потоками происходит не сразу, а по мере необходимости. Для этого определяется операция $ fork(a, b) $ которой передается поток $ a $ который решает какую-то подзадачу DPPL. И поток b который в данный момент свободен.

Ниже приводится псевдокод алгоритма fork который разделяет задачу решателя f на две.

%\begin{singlespacing}
%\begin{algorithm}[H]
%\KwData{ $f$, $t$ - sat machines}
%        copy all information from f to t \;
%        \For  {$i \in [0, frameSize]$} {
%            var = literalToVar(f.frame(i))\;
%            \If {f.reason[var] == GUESSED} {
%                f.reason[var] = -1\;
%                \While{t.reason[var] == GUESSED}{
%                    t.rollback()\;
%                }
%                \Return \;
%            }
%        }            
%\caption{Алгоритм Fork.}
%\end{algorithm}
%\end{singlespacing}

\begin{singlespacing}
\textbf{Функция} fork($f, t$)
\begin{algorithmic}[1]
\STATE  $t \leftarrow f$
\FOR{$i \in [0, frameSize]$} 
	\STATE var $\leftarrow$ literalToVar(f.frame(i))
	\IF{f.reason[var] = GUESSED}
		\STATE f.reason[var] = ROLLBACK
		\WHILE{t.reason[var] = GUESSED}
			\STATE t.rollback()
		\ENDWHILE
		\RETURN  
	\ENDIF
\ENDFOR
\end{algorithmic}
\end{singlespacing}

\begin{figure}[H]
	\centering
	\includegraphics[width=80mm]{pics/Forks.pdf}
	\caption{Схема работы балансировки}
	\label{fig:fork}
\end{figure}

Алгоритм распараллеливания выглядит следующим образом:

\begin{singlespacing}
\textbf{Функция} Parallel DPLL()
\begin{algorithmic}[1]
\STATE  solvers[0].init()
\WHILE{has working solvers(solvers)}
	\FOR{$solver \in solvers$} 
		\STATE solver.make DPLL step()
		\IF{solver.state = SAT}
			\RETURN  solver.variables	
		\ENDIF
	\ENDFOR
	\IF{has free solvers(solvers)}
		\STATE do fork()
	\ENDIF
\ENDWHILE
\end{algorithmic}
\end{singlespacing}


\begin{itemize}
\item
	Инициализируем один из потоков. Все остальные переводятся в состояние UNSAT.
\item
	Пока работает хоть одни поток.
\item 
	Выполняем один шаг каждого потока.
\item
	Если есть свободные потоки, то выполняем операцию fork для того что бы заполнить их.
\end{itemize}

Как правило при оптимизации алгоритмов при помощи CUDA большая часть алгоритма реализуется на CPU. Только  занимающая большую часть времени функция (bottle neck) реализуется на GPU.  Применительно к методу разделяй и властвуй такой подход не работает. Для работы алгоритма требуется значительно количество памяти, порядка число переменных умножить на число потоков. Если часть алгоритма DPLL реализована на CPU, то будет тратиться значительное время на пересылку данных. В связи с этим вся процедура DPPL была полностью реализована на CUDA.

\subsection{Улучшенный метод разделяй и властвуй}

Если реализовать всю процедуру DPLL в одном ядре, то программа покажет крайне низкую производительность. Это связано с тем что CUDA является SIMD архитектурой. Для эффективного исполнения ядро CUDA должно содержать как можно меньше операций ветвления. Для того чтобы получить прирост производительности алгоритм DPLL требуется разбить на части каждую из которых реализовать в отдельном ядре. Для того что бы разделить процедуру DPLL на несколько ядер, алгоритм DPLL был записан в виде конечного автомата.

\begin{center}
\includegraphics[width=170mm]{pics/fsm.pdf}
\end{center}

Распишем подробнее действия выполняемые в каждом состоянии.

\begin{itemize}
\item
	\textbf{SAT} --- формула является выполнимой. Вернуть текущую подстановку.
\item
	\textbf{UNSAT} --- формула является невыполнимой.
\item
	\textbf{Присвоение переменной значения} --- В формуле не осталось единичных или пустых дизъюнктов. Требуется выбрать переменную и присвоить ей значение ноль или один. После чего положить это значение в стек.
\item
	\textbf{Откат} --- Был обнаружен конфликт. Достаем из стека все переменные. Для каждой переменной устанвливаем значение $UNASSIGNED$. Пока не дойдем до переменной $v$ для которой $reason(v) == GUESSED$. Изменяем значение переменной на противоположное. Устанавливаем $reason(v) := ROLLBACK$.
\item
	\textbf{Анализ формулы} --- На данном шаге алгоритм ищет единичные дизъюнкты. 
Для того чтобы не перебирать все дизъюнкты в формуле мы просматриваем только те дизъюнкты которые изменялись. Алгоритм использует переменную lastWatched, которая указывает на еще не просмотренную часть стека. 
Для того что бы найти единичные или пустые дизъюнкты мы посматриваем все дизъюнкты 
\end{itemize}

В данном автомате операции выполняемые с состояниях "Присвоение переменной значения",  "Откат", "Анализ формулы"  можно реализовать в своем ядре. Так же операцию разделения потоков требуется перенести на CUDA.

Ниже приводится псевдокод алгоритма при таком походе.

\begin{singlespacing}
\textbf{Функция} DPLL()

\begin{algorithmic}[1]
\REPEAT
	\STATE setFreeVariablesCUDA()
	\STATE propagateUnitsCUDA()
	\STATE doRollbacksCUDA()
	\STATE loadStates()
	\FOR{$s \in solvers$} 
		\IF{s has SAT state}
			\RETURN s.values()
		\ENDIF	
	\ENDFOR
	\IF{has free solvers}
		\STATE doAllForksСUDA()
	\ENDIF
\UNTIL {no working solvers} 
\RETURN UNSAT

\end{algorithmic}
\end{singlespacing}

Каждя из функций  setFreeVariablesCUDA(), propagateUnitsCUDA(), doRollbacksCUDA() выполняется на всех решателях, если решатель находится в неподходящем состоянии функция сразу завершается. Функция propagateUnitsCUDA() исследования реализации показали что больше всего времени занимате функция propagateUnitsCUDA() в которой выполняется анализ формулы. 

\subsection{Параллельный поиск единичных дизъюнктов}

Большую часть времени работы алгоритма занимает операция  "Анализ формулы" так что в первую очередь было реализовано параллельное удаление единичных дизъюнктов.
Проверка каждого дизъюнкта выполняется параллельно. Для этого требуется записать номера всех дизъюнктов в массив, после чего для каждого элемента массива запустить поток. Возникает проблема как записать все номера задач параллельно, так как каждый решатель может проверить разное число дизъюнктов решатель $ i + 1 $ не знает где заканчиваются данные решателя $ i $. Для того что бы вычислить смещения выполняется следующая операция: 
\begin{itemize}
\item
.	Для каждого потока вычисляется количество дизъюнктов которое требуется проверить.
\item
	Для получившегося массива считается префиксная сумма. В получившимся массиве для каждого решателя указано смещение с которого требуется записывать задачи.
\item
	Используя данный массив, создается список задач которые требуется выполнить
\item
	Каждая задача выполняется в своем потоке
\item
	Данные со всех задач собираются и обрабатываются
\end{itemize}


\begin{figure}[H]
	\centering
	\includegraphics[width=160mm]{pics/Balance.pdf}
	\caption{Схема заполнения массива задач на основе префиксной суммы}
	\label{fig:balance}
\end{figure}


\subsection{Параллельная реализация Look Ahead}

Эвристика Look-Ahead довольно проста в реализации на CUDA. Качество переменной $x$ для расщепления формулы оценивается как количество новых переменных выводимых, при подстановке переменной $x$ в формулу. Для того что бы это вычислить запускается модифицированная операция анализа формулы. Ей добавляется новый параметр,
значение переменной $x$. Ниже написан псевдокод операции вычисления веса переменной. Так в данном алгоритме  мало информации передается GPU, большую часть алгоритма можно реализовать на CPU. 

Ниже приводится псевдокод функции для проверки дизъюнкта 

\begin{singlespacing}
\textbf{Функция} updateClause(clause, settedLiteral, varValues)

\begin{algorithmic}[1]
\STATE  unit = -1
\FOR{$literal \in clause$} 
	\STATE solver.make DPLL step()
	\IF{(literalToVar(literal) != literalToVar(settedLiteral)}
		\STATE  value = varValues[literalToVar(literal)];
	\ELSE
		\STATE  value = settedLiteral;
	\ENDIF

	\IF{value != 0}
		\IF{value == literal}
			\RETURN 0
		\ENDIF
	\ELSE
		\IF{unit != -1}
			\RETURN 0
		\ELSE
			\STATE unit = 1;
		\ENDIF
		
	\ENDIF
	\RETURN unit
\ENDFOR

\end{algorithmic}
\end{singlespacing}

Каждая переменная обрабатывается в отдельном потоке. Однако возникает проблема в том что в формуле может быть слишком мало переменных, а так же части переменным будет присвоено значение, и как следствие, будет запущено слишком мало потоков. Для решенная данной проблемы метод Look-Ahead был объединен с методом разделяй и властвуй. 

\subsection{Изучение новых дизъюнктов}

Для изучения новых дизъюнктов к алгоритму разделяй и властвуй требуется добавить еще одно ядро, которое будет заниматься вычислением новых дизъюнктов. Ниже привевен псевдокод функции, выполняющей операцию анализа конфликта.

\begin{singlespacing}
\textbf{Функция} doBackTrack() 
\begin{algorithmic}[1]
    \STATE fill(done,  0)
    \FOR {i $\in$ [frameSize - 1; 0];} 
        \STATE var = literalToVar(frame[i])
        \IF {is clause (reasons[var])}
            \STATE break
        \ENDIF
        \STATE last[var] = true      
    \ENDFOR
    \STATE newClause.size = 0
    \FOR {l $\in$ conflicClause}
	\STATE stack.push(literal)
        	\STATE done[literalToVar(literal)] = true
    \ENDFOR
    \WHILE {stack.size > 0} 
        \STATE literal = stack.pop()
        \IF {(last[lliteralToVar(literal)]}
            \STATE newClause.add(literal xor 1)
            \IF {newClause.size > MAX NEW VAR SIZE} 
                \RETURN
            \ENDIF
        \ELSE
	\STATE reason = reasons[literalToVar(literal)]
	\FOR {l $\in$ reason}                     
                \IF {!(done[var >> 1])} 
                    \STATE stack.push(l xor 1)
                    \STATE done[literalToVar(l)] = true
                \ENDIF
            \ENDFOR
        \ENDIF
    \ENDWHILE
\end{algorithmic}
\end{singlespacing}

Так как новые дизъюнкты занимают мало памяти их можно легко передать на CPU. Все найденные дизъюнкты проверяются на дублирование, так как может быть найдено несколько одинаковых дизъюнктов. После чего дизъюнкты склавдываются в очередь. Когда в очереди набираестя достатончое количество дизъюнктов, они добавляются к формуле, массив watches пересчитывается. Далее массив содержащий формулу отправляется на видеокарту. После чего происходит операци согласования состояния решателей и новой формулы. Данная операция для каждого решателя проверяет нет ли пустых или единичных дизъюнктов. Данная операция по своей сути аналонична операции анализа формулы, за исключением того что в ней проверяются все новые дизъюнкты. Ниже псевдокод данной операции.

\begin{singlespacing}
\begin{lstlisting}[language=C++]

__global__
void addNewClauses(int oldSize, int clausesNumber) {
    int m = blockIdx.x * THREADS_PER_BLOCK_SMALL + threadIdx.x;
    if (m >= MAX_PROCESSES) {
        return;
    }

    CudaSolver solver(m);
    if (solver.isWorking()) {
        for (int i = oldSize - 1; i < clausesNumber - 1; i++) {
            int var = tex1Dfetch(clauses_tex, i);
            if (var == -1) {
                int c;
                do {
                    c = calculateUnit(i + 1, data.variables + m * data.varsNumber);
                    if (c != -2) {
                        if (c == -1) {
                            if (!solver.doRollback()) {
                                break;
                            }
                        } else {
                            solver.setVarValue(c, i + 1);
                        }
                    }
                } while (c == -1);
            }
        }
    }
}

\end{lstlisting}
\end{singlespacing}



\begin{figure}[H]
	\centering
	\includegraphics[width=170mm]{pics/fsm2.pdf}
	\caption{Автомат для DPLL с изучением новыз дизъюнктов}
	\label{fig:dpll_learning}
\end{figure}


\pagebreak

\section{Результаты}

Был проведен ряд тестов для сравнения ускорения даваемого CUDA. А так же для сравнения эффективности методов. Для сравнения использовался компьютер со следующими характеристиками:
\begin{itemize}
\item
	CPU - 3.2 Ghz
\item
	Видеокарта NVIDIA GeForce 9800 GT с семью мультипроцессорами.
\end{itemize}

Для тестирования использовалось подмножество тестов с сайта соревновании по SAT (\url{http://www.satcompetition.org/}).

Количество переменных в формуле варьируется от 30 до 500. Количетсво дизъюнктов в формуле варьируется от 100 до 5000. 

\subsection{Формат DIMACS CNF}

Каждая булева формула, как было описано в Главе 1, может быть преобразована в конъюнктивную нормальную форму. Для того что бы стандартизировать запись формул для решателей SAT был разработан формат \textit{DIMACS CNF}. Файл в формате 
\textit{DIMACS CNF} является текстовый файлом со следующей структурой.

Каждая строка начинающаяся с символа  "c" является комментарием. Первая строка не комментарий должна быть записана в виде:

\texttt{ p cnf [ЧИСЛО ПЕРЕМЕННЫХ] [ЧИСЛО ДИЗЪЮНКТОВ]}

Каждая последующая строка, которая не является комментарием определяет дизъюнкт. Дизъюнкт записывается как последовательность чисел записанных через пробел, положительно значение обозначает соответствующую переменную  (4 значит $x4$), и отрицательное значение значит отрицание переменной  (-5 значит $\neg x5$). Каждая строка должна заканчиваться числом ноль.

$$  (x1 \vee  \neg x5 \vee  x4) \wedge  (\neg x1 \vee  x5 \vee  x3 \vee  x4) \wedge (\neg x3 \vee  \neg x4) $$

Формула представленная выше будет записана как:

\texttt{c Это комментарий.}

\texttt{p cnf 5 3}

\texttt{1 -5 4 0}

\texttt{-1 5 3 4 0}

\texttt{-3 -4 0}



\subsection{Сравнение реализаций различных подходов для CPU и CUDA}
    Сравнение времени работы простого алгоритма DPLL на CPU и алгоритма DPLL на CUDA.

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/SimpleVsCpu.pdf}
	\caption{Сравнение времени работы алгоритма DPLL на CPU и на CUDA.}
	\label{fig:SimpleVsCpu}
\end{figure}

На данном рисунке каждая точка означает некторорый тест. По оси $ X $ отложено время работы алгоритма написанного на CUDA. По оси $Y$ отложено время работы алогоритма на CPU. Вожно соотношение этих величин, которое отражается углом под которым находится точка. Чем ближе точка находится к оси Y, тем больше ускорение.

    Сравнение времени работы алгоритма look-Ahead на CPU и алгоритма look-Ahead на CUDA.

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/LookAheadVsCpu.pdf}
	\caption{Сравнение времени работы алгоритма DPLL look-ahead на CPU и на CUDA.}
	\label{fig:LookAheadVsCpu}
\end{figure}  

    Сравнение времени работы алгоритма DPLL с изучением новых диъюнктов с реализацией на CPU

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/LearnVsCpu.pdf}
	\caption{Сравнение времени работы алгоритма DPLL c изучение новых дизъюнктов на CPU и на CUDA.}
	\label{fig:LookAheadVsCpu}
\end{figure}

На рис.~\ref{fig:Histogram} приводится сводная гистограмма для ускорений различных методов.

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/Histogram.pdf}
	\caption{Сравнения ускорения различных подходов}
	\label{fig:Histogram}
\end{figure}

\subsection{Сравнение метода разделяй и властвуй c look-ahead}

    Сравнение времени работы простого алгоритма и алгоритма Look-Ahead на CUDA.

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/SimpleVsLookAhead.pdf}
	\caption{Сравнение времени работы алгоритма DPLL и алгоритма DPLL look-ahead}
	\label{fig:SimpleVsLookAhead}
\end{figure}

\subsection{Сравнение метода look-ahead с MiniSat}
    Сравнение времени работы MiniSat и алгоритма Look-Ahead на CUDA.   

\begin{figure}[H]
	\centering
	\includegraphics[width=120mm]{pics/LookAheadVsMiniSat.pdf}
	\caption{Сравнение времени работы алгоритма DPLL look-ahead, реализованного на CUDA и решателя MiniSat}
	\label{fig:LookAheadVsMiniSat}
\end{figure}

\subsection{Выводы}

Были опробованны несколько подходов к реализации алгоритма DPLL на CUDA. Расмотртим какой приросто производительности был получен при использований каждого алгоритма.

    \begin{center}
	\begin{tabular}{|l|l|l|l|}
	\hline
	\multirow{2}{*}{алгоритм} & cреднее & максимальное & тестов \\
	 & ускорение  & ускорение &  пройдено \\
	\hline
	DPLL & 2.6 & 9 & 231 / 433\\
	 Look-Ahead & 4.8 & 6 & 312 / 433 \\
	 Обучающийся & 3.2 & 7 & 286 / 433 \\
	 \hline
     	\end{tabular}
    \end{center}

Рассмотририм особенности каждого из подходов:

\begin{itemize}
\item
	Разделяй и властвуй. Самый простойтой алогоритм. Позволяетм рассмотреть общие особенности реализации DPLL.
\item
	Разделяй и властвуй с изучением новых дизъюнктов. Показывает неплохие результаты, однако данный алгоритм сложен в реализации и сложен для внесения каких-либо изменений.
\item
	Разделяй и властвуй с look-ahead. Данный алгоритм показывает самые хорошие результаты. Так же он прост в реализации и легко модифицируем.
\end{itemize}

Из всех алгоритмов наилучшие результаты показал Look-Ahead. Из чего можно сделать вывод что данный алгоритм наиболее пригоден для реализации на CUDA. Так же данной работой не были охвачены алгоритмы совмещаюшие вычисления на видеокарте с вычмслениями на CPU. Данный подход так же может дать существенный прирост производительности.

\pagebreak

\renewcommand{\refname}{Список литературы}
\addcontentsline{toc}{section}{Список литературы}
\bibliographystyle{gost71s}
\bibliography{library}

\end{document}
